Nuprl Lemma : derived-seq_wf
11,40
postcript
pdf
T
:Type,
f
:(
T
),
s
:(
k
:
({0..
k
}
)). derived-seq(
f
;
s
)
(
k
:
({0..
k
}
T
))
latex
Definitions
Type
,
t
T
,
,
x
:
A
B
(
x
)
,
{
x
:
A
|
B
(
x
)}
,
x
:
A
.
B
(
x
)
,
#$n
,
{
i
..
j
}
,
x
:
A
B
(
x
)
,
f
(
a
)
,
n
+
m
,
a
<
b
,
Void
,
P
Q
,
False
,
A
,
P
&
Q
,
A
B
,
i
j
<
k
,
,
x
.
A
(
x
)
,
<
a
,
b
>
,
let
x
,
y
=
A
in
B
(
x
;
y
)
,
derived-seq(
f
;
s
)
Lemmas
int
seg
wf
,
nat
wf
origin
T:Type, f:(
T), s:(k: 
({0..k
})). derived-seq(f;s) 
(k: ({0..k}T)) T:Type, f:(T), s:(k: ({0..k})). derived-seq(f;s) (k: ({0..k}T)) TB(x)x:A. B(x)} B(x)
Q
A
B j < k
x.A(x)